/LMAR=0/XLINE=3/FONT#0=BAXL30/FONT#1=BDR30/FONT#2=BAXM30/FONT#3=BASB30/FONT#4=BDR30/FONT#5=SUB/FONT#6=SUP/FONT#9=FIX40/FONT#10=FIX30/FONT#11=GRFX25/FONT#12=GRFX35
␈↓ ↓H␈↓␈↓ εP␈↓ I1


␈↓ ↓H␈↓β␈↓ ¬yCHAPTER I

␈↓ ↓H␈↓β␈↓ ∧0PROVING LISP PROGRAMS CORRECT




␈↓ ↓H␈↓        In␈α∪this␈α∪chapter␈α∩we␈α∪will␈α∪introduce␈α∩techniques␈α∪for␈α∪proving␈α∩LISP␈α∪programs␈α∪correct.␈α∩ The
␈↓ ↓H␈↓techniques␈α
will␈α
mainly␈α
be␈α
limited␈α
to␈α
what␈α∞we␈α
may␈α
call␈α
␈↓αclean␈↓␈α
LISP␈α
programs.␈α
 In␈α∞particular,␈α
there
␈↓ ↓H␈↓must␈α∞be␈α∞no␈α
side␈α∞effects,␈α∞because␈α
our␈α∞methods␈α∞depend␈α
on␈α∞the␈α∞ability␈α
to␈α∞replace␈α∞subexpressions␈α
by
␈↓ ↓H␈↓equal expressions.

␈↓ ↓H␈↓        The␈α
 necessary␈α
basic␈α
facts␈α
can␈α
be␈α
divided␈α
into␈α
several␈α
categories:␈α
first␈α
order␈α
logic␈α
including
␈↓ ↓H␈↓conditional␈αforms␈αand␈αfirst␈αorder␈αlambda-expressions,␈αalgebraic␈αfacts␈αabout␈αlists␈αand␈αS-expressions,
␈↓ ↓H␈↓facts␈α∂about␈α∂the␈α∂inductive␈α∂structure␈α∂of␈α∂lists␈α∂and␈α∂S-expressions,␈α∂and␈α∂general␈α∂facts␈α⊂about␈α∂functions
␈↓ ↓H␈↓defined␈α⊃by␈α⊃recursion.␈α⊂ Ideally,␈α⊃we␈α⊃would␈α⊃use␈α⊂a␈α⊃general␈α⊃theory␈α⊂of␈α⊃recursive␈α⊃definition␈α⊃to␈α⊂prove
␈↓ ↓H␈↓theorems␈αabout␈αLISP␈αfunctions.␈α However,␈αthe␈αgeneral␈αtheory␈αis␈αnot␈αwell␈αenough␈αdeveloped,␈αso␈αwe
␈↓ ↓H␈↓have␈α⊂had␈α∂to␈α⊂introduce␈α⊂some␈α∂methods␈α⊂limited␈α⊂to␈α∂LISP␈α⊂functions␈α⊂defined␈α∂by␈α⊂particular␈α⊂kinds␈α∂of
␈↓ ↓H␈↓recursion schemes.



␈↓ ↓H␈↓1.  ␈↓βFirst order logic with conditional forms and lambda-expressions.␈↓


␈↓ ↓H␈↓        The␈α⊂logic␈α⊂we␈α⊂shall␈α⊂use␈α⊂is␈α⊂called␈α⊂first␈α⊂order␈α⊂logic␈α⊂with␈α⊂equality,␈α⊂but␈α⊂we␈α⊂will␈α⊂extend␈α⊂it␈α⊂by
␈↓ ↓H␈↓allowing␈α
conditional␈α
forms␈αto␈α
be␈α
terms␈αand␈α
lambda-expressions␈α
to␈αbe␈α
function␈α
expressions.␈α From
␈↓ ↓H␈↓the␈α∂mathematical␈α⊂point␈α∂of␈α⊂view,␈α∂these␈α⊂extensions␈α∂are␈α∂inessential,␈α⊂because,␈α∂as␈α⊂we␈α∂shall␈α⊂see,␈α∂every
␈↓ ↓H␈↓sentence␈αthat␈αincludes␈αconditional␈αforms␈αor␈αfirst␈αorder␈αlambdas␈αcan␈αreadily␈αbe␈αtransformed␈αinto␈αan
␈↓ ↓H␈↓equivalent␈αsentence␈αwithout␈αthem.␈α However,␈αthe␈αextensions␈αare␈αpractically␈αimportant,␈αbecause␈αthey
␈↓ ↓H␈↓permit␈α
us␈α
to␈α
use␈α
certain␈α
recursive␈α∞definitions␈α
directly␈α
as␈α
formulas␈α
of␈α
the␈α
logic.␈α∞ Unfortunately,␈α
we
␈↓ ↓H␈↓will␈α
not␈αbe␈α
able␈α
to␈αtreat␈α
all␈α
recursive␈αdefinitions␈α
in␈αthis␈α
system,␈α
but␈αonly␈α
those␈α
which␈αwe␈α
can␈αbe␈α
sure
␈↓ ↓H␈↓are␈α∂defined␈α∞for␈α∂all␈α∞values␈α∂of␈α∞the␈α∂arguments.␈α∞ Moreover,␈α∂we␈α∞will␈α∂be␈α∞unable␈α∂to␈α∂prove␈α∞definedness
␈↓ ↓H␈↓within␈α∞the␈α
system,␈α∞so␈α∞we␈α
will␈α∞be␈α∞restricted␈α
to␈α∞classes␈α
of␈α∞recursive␈α∞definitions␈α
which␈α∞we␈α∞can␈α
prove
␈↓ ↓H␈↓always␈α
defined␈α
by␈α
an␈α
argument␈α∞outside␈α
the␈α
system.␈α
 Fortunately,␈α
many␈α
interesting␈α∞LISP␈α
functions
␈↓ ↓H␈↓meet␈α∂these␈α∂restrictions␈α∂including␈α⊂all␈α∂the␈α∂important␈α∂functions␈α∂so␈α⊂far␈α∂used␈α∂except␈α∂for␈α∂␈↓αeval␈↓␈α⊂and␈α∂its
␈↓ ↓H␈↓variants.

␈↓ ↓H␈↓        Formulas␈α⊂of␈α⊂the␈α⊂logic␈α⊂are␈α⊂built␈α⊂from␈α⊂constants,␈α⊂variables␈α⊂predicate␈α⊂symbols,␈α⊂and␈α∂function
␈↓ ↓H␈↓symbols␈α⊃using␈α⊃function␈α∩application,␈α⊃conditional␈α⊃forms,␈α∩boolean␈α⊃forms,␈α⊃lambda␈α∩expressions,␈α⊃and
␈↓ ↓H␈↓quantifiers.

␈↓ ↓H␈↓␈↓βConstants␈↓:␈α∂We␈α∂will␈α∂use␈α∂S-expresssions␈α∂as␈α∞constants␈α∂standing␈α∂for␈α∂themselves␈α∂and␈α∂also␈α∂lower␈α∞case
␈↓ ↓H␈↓letters␈α∪from␈α∪the␈α∪first␈α∀part␈α∪of␈α∪the␈α∪alphabet␈α∪to␈α∀represent␈α∪constants␈α∪in␈α∪other␈α∪domains␈α∀than␈α∪S-
␈↓ ↓H␈↓expressions.

␈↓ ↓H␈↓␈↓βVariables␈↓: We will use the letters ␈↓αu␈↓ thru ␈↓αz␈↓ with or without subscripts as variables.
␈↓ ↓H␈↓␈↓ ¬wCHAPTER I␈↓ I2


␈↓ ↓H␈↓␈↓βFunction␈αsymbols␈↓:␈αThe␈αletters␈α␈↓αf␈↓,␈α␈↓αg␈↓␈αand␈α␈↓αh␈↓␈αwith␈αor␈αwithout␈αsubscripts␈αare␈αused␈αas␈αfunction␈αsymbols.
␈↓ ↓H␈↓The␈αLISP␈αfunction␈αsymbols␈α␈↓βa␈↓,␈α␈↓βd␈↓␈α
and␈α.␈α(as␈αan␈αinfix)␈αare␈α
also␈αused␈αas␈αfunction␈αsymbols.␈α We␈α
suppose
␈↓ ↓H␈↓that each function symbol takes the same definite number of arguments every time it is used.

␈↓ ↓H␈↓␈↓βPredicate␈αsymbols␈↓:␈αThe␈αletters␈α␈↓αp␈↓,␈α␈↓αq␈↓␈αand␈α␈↓αr␈↓␈αwith␈αor␈αwithout␈αsubscripts␈αare␈αused␈αas␈αpredicate␈α
symbols.
␈↓ ↓H␈↓We␈α
will␈α
also␈α
use␈α
the␈αLISP␈α
predicate␈α
symbol␈α
␈↓βat␈↓␈α
as␈αa␈α
constant␈α
predicate␈α
symbol.␈α
 The␈αequality␈α
symbol
␈↓ ↓H␈↓=␈αis␈αalso␈αused␈αas␈αan␈αinfix.␈α We␈αsuppose␈αthat␈αeach␈αpredicate␈αsymbol␈αtakes␈αthe␈αsame␈αdefinite␈αnumber
␈↓ ↓H␈↓of arguments each time it is used.

␈↓ ↓H␈↓        Next␈α
we␈α
define␈α
terms,␈α
sentences,␈α
function␈α
expressions␈α
and␈α
predicate␈α
expressions␈αinductively.
␈↓ ↓H␈↓A␈αterm␈α
is␈αan␈α
expression␈αwhose␈α
value␈αwill␈α
be␈αan␈αobject␈α
like␈αan␈α
S-expression␈αor␈α
a␈αnumber␈α
while␈αa
␈↓ ↓H␈↓sentence␈α
has␈α
value␈α
␈↓∧T␈↓␈α
or␈α␈↓∧F␈↓.␈α
 Terms␈α
are␈α
used␈α
in␈α
making␈αsentences,␈α
and␈α
sentences␈α
occur␈α
in␈α
terms␈αso
␈↓ ↓H␈↓that␈α∀the␈α∀definitions␈α∀are␈α∀␈↓αmutually␈α∀recursive␈↓␈α∃where␈α∀this␈α∀use␈α∀of␈α∀the␈α∀word␈α∀␈↓αrecursive␈↓␈α∃should␈α∀be
␈↓ ↓H␈↓distinguished␈α⊃from␈α⊃its␈α⊃use␈α⊃in␈α⊃recursive␈α⊃definitions␈α⊃of␈α⊃functions.␈α⊃ Function␈α⊃expressions␈α⊃are␈α⊃also
␈↓ ↓H␈↓involved in the mutual recursion.

␈↓ ↓H␈↓␈↓βTerms␈↓:␈α∩Constants␈α⊃are␈α∩terms,␈α⊃and␈α∩variables␈α⊃are␈α∩terms.␈α⊃ If␈α∩␈↓αf␈↓␈α⊃is␈α∩a␈α⊃function␈α∩expression␈α∩taking␈α⊃␈↓αn␈↓
␈↓ ↓H␈↓arguments,␈αand␈α␈↓αt␈↓¬1␈↓α, ... ,t␈↓¬n␈↓α␈↓␈αare␈αterms,␈αthen␈α␈↓αf[t␈↓¬1␈↓α, ... ,t␈↓¬n␈↓α]␈↓␈αis␈αa␈αterm.␈α If␈α␈↓αp␈↓␈αis␈αa␈αsentence␈αand␈α␈↓αt␈↓¬1␈↓α␈↓␈αand␈α
␈↓αt␈↓¬2␈↓
␈↓ ↓H␈↓are␈α∂terms,␈α∞then␈α∂␈↓βif␈↓α p ␈↓βthen␈↓α t␈↓¬1␈↓α ␈↓βelse␈↓α t␈↓¬2␈↓␈α∞is␈α∂a␈α∞term.␈α∂ We␈α∞soften␈α∂the␈α∞notation␈α∂by␈α∞allowing␈α∂infix␈α∞symbols
␈↓ ↓H␈↓where this is customary.

␈↓ ↓H␈↓␈↓βSentences␈↓:␈α∩If␈α⊃␈↓αp␈↓␈α∩is␈α⊃a␈α∩predicate␈α⊃expression␈α∩taking␈α⊃␈↓αn␈↓␈α∩arguments␈α⊃and␈α∩␈↓αt␈↓¬1␈↓α, ... ,t␈↓¬n␈↓α␈↓␈α⊃are␈α∩terms,␈α⊃then
␈↓ ↓H␈↓␈↓αp[t␈↓¬1␈↓α, ... ,t␈↓¬n␈↓α]␈↓␈αis␈αa␈αsentence.␈α Equality␈αis␈αalso␈αused␈αas␈αan␈αinfixed␈αpredicate␈αsymbol␈αto␈αform␈α
sentences,
␈↓ ↓H␈↓i.e.␈α
␈↓αt␈↓¬1␈↓α = t␈↓¬2␈↓␈α
is␈α
a␈α
sentence.␈α
 If␈α
␈↓αp␈↓␈α
is␈α
a␈α
sentence,␈αthen␈α
␈↓α¬p␈↓␈α
is␈α
also␈α
a␈α
sentence.␈α
 If␈α
␈↓αp␈↓␈α
and␈α
␈↓αq␈↓␈α
are␈αsentences,
␈↓ ↓H␈↓then␈α␈↓αp∧q␈↓,␈α␈↓αp∨q␈↓,␈α␈↓αp⊃q␈↓,␈αand␈α␈↓αp≡q␈↓␈αare␈αsentences.␈α If␈α␈↓αp␈↓,␈α␈↓αq␈↓␈αand␈α␈↓αr␈↓␈αare␈αsentences,␈αthen␈α␈↓βif␈↓α p ␈↓βthen␈↓α q ␈↓βelse␈↓α r␈↓␈αis␈αa
␈↓ ↓H␈↓sentence.␈α⊃ If␈α⊃␈↓αx␈↓¬1␈↓α, ..., x␈↓¬n␈↓α␈↓␈α⊃are␈α∩variables,␈α⊃and␈α⊃␈↓αp␈↓␈α⊃is␈α⊃a␈α∩term,␈α⊃then␈α⊃␈↓α∀x␈↓¬1␈↓α ... x␈↓¬n␈↓α:t␈↓␈α⊃and␈α∩␈↓α∀x␈↓¬1␈↓α ... x␈↓¬n␈↓α:t␈↓␈α⊃are
␈↓ ↓H␈↓sentences.

␈↓ ↓H␈↓␈↓βFunction␈α∂expressions␈↓:␈α∂A␈α∞function␈α∂symbol␈α∂is␈α∞a␈α∂function␈α∂expression.␈α∞ If␈α∂␈↓αx␈↓¬1␈↓α, ... ,x␈↓¬n␈↓α␈↓␈α∂are␈α∞variables
␈↓ ↓H␈↓and ␈↓αt␈↓ is a term, then ␈↓α[λx␈↓¬1␈↓α, ... ,x␈↓¬n␈↓α:t]␈↓ is a function expression.

␈↓ ↓H␈↓␈↓βPredicate␈α
expressions␈↓:␈α
A␈α
predicate␈αsymbol␈α
is␈α
a␈α
predicate␈αexpression.␈α
 If␈α
␈↓αx␈↓¬1␈↓α, ... ,x␈↓¬n␈↓α␈↓␈α
are␈αvariables
␈↓ ↓H␈↓and ␈↓αp␈↓ is a sentence, then ␈↓α[λx␈↓¬1␈↓α, ... ,x␈↓¬n␈↓α:p]␈↓ is a predicate expression.

␈↓ ↓H␈↓        An␈α
occurrence␈α
of␈αa␈α
variable␈α
␈↓αx␈↓␈αis␈α
called␈α
bound␈αif␈α
it␈α
is␈αin␈α
an␈α
expression␈αof␈α
one␈α
of␈α
the␈αforms
␈↓ ↓H␈↓␈↓α[λx␈↓¬1␈↓α ... x␈↓¬n␈↓α:t]␈↓,␈α␈↓α[λx␈↓¬1␈↓α ... x␈↓¬n␈↓α:p]␈↓,␈α␈↓α[∀x␈↓¬1␈↓α ... x␈↓¬n␈↓α:p]␈↓␈αor␈α␈↓α[∃x␈↓¬1␈↓α ... x␈↓¬n␈↓α:p]␈↓␈αwhere␈α␈↓αx␈↓␈αis␈αone␈αof␈αthe␈αnumbered␈α␈↓αx␈↓'s.␈α If
␈↓ ↓H␈↓not bound an occurrence is called free.

␈↓ ↓H␈↓        The␈α∞␈↓αsemantics␈↓␈α
of␈α∞first␈α
order␈α∞logic␈α
consists␈α∞of␈α∞the␈α
rules␈α∞t~at␈α
enable␈α∞us␈α
to␈α∞determine␈α∞when␈α
a
␈↓ ↓H␈↓sentence␈αis␈αtrue␈α
and␈αwhen␈αit␈αis␈α
false.␈α However,␈αthe␈αtruth␈α
or␈αfalsity␈αof␈αa␈α
sentence␈αis␈αrelative␈α
to␈αthe
␈↓ ↓H␈↓interpretation␈αassigned␈αto␈αthe␈αconstants,␈αthe␈α
function␈αand␈αpredicate␈αsymbols␈αand␈αthe␈α
free␈αvariables
␈↓ ↓H␈↓of the formula.  We proceed as follows:

␈↓ ↓H␈↓        We␈α
begin␈α
by␈αchoosing␈α
a␈α
domain.␈α In␈α
most␈α
cases␈αwe␈α
shall␈α
consider␈αthe␈α
domain␈α
will␈αinclude␈α
the
␈↓ ↓H␈↓S-expressions␈αand␈αany␈αS-expression␈αconstants␈αappearing␈αin␈αthe␈αformula␈αstand␈αfor␈αthemselves.␈α We
␈↓ ↓H␈↓will␈α
allow␈α∞for␈α
the␈α∞possibility␈α
that␈α∞other␈α
objects␈α
than␈α∞S-expressions␈α
exist,␈α∞and␈α
some␈α∞constants␈α
may
␈↓ ↓H␈↓designate␈α⊂them.␈α⊂ Each␈α⊂function␈α⊂or␈α⊂predicate␈α⊃symbol␈α⊂is␈α⊂assigned␈α⊂a␈α⊂function␈α⊂or␈α⊂predicate␈α⊃on␈α⊂the
␈↓ ↓H␈↓␈↓ ¬wCHAPTER I␈↓ I3


␈↓ ↓H␈↓domain.␈α↔ We␈α⊗will␈α↔normally␈α⊗assign␈α↔to␈α⊗the␈α↔basic␈α⊗LISP␈α↔function␈α⊗and␈α↔predicate␈α↔symbols␈α⊗the
␈↓ ↓H␈↓corresponding␈αbasic␈αLISP␈αfunctions␈αand␈αpredicates.␈α Each␈αvariable␈αappearing␈αfree␈αin␈αa␈αsentence␈αis
␈↓ ↓H␈↓also␈αassigned␈αan␈αelemet␈αof␈αthe␈αdomain.␈α All␈αthese␈αassignments␈αconstitute␈αan␈αinterpretation,␈αand␈αthe
␈↓ ↓H␈↓truth of a sentence is relative to the interpretation.

␈↓ ↓H␈↓        The␈α⊃truth␈α⊃of␈α⊂a␈α⊃sentence␈α⊃is␈α⊃determined␈α⊂from␈α⊃the␈α⊃values␈α⊂of␈α⊃its␈α⊃constituents␈α⊃by␈α⊂evaluating
␈↓ ↓H␈↓successively␈α∂larger␈α∂subexpressions.␈α⊂ The␈α∂rules␈α∂for␈α⊂handling␈α∂functions␈α∂and␈α⊂predicates,␈α∂conditional
␈↓ ↓H␈↓expressions,␈α
equality,␈α
and␈α
Boolean␈α
expressions␈αare␈α
exactly␈α
the␈α
same␈α
as␈αthose␈α
we␈α
have␈α
used␈α
in␈αthe
␈↓ ↓H␈↓previous chapters.  We need only explain quantifiers:

␈↓ ↓H␈↓        ␈↓α∀x␈↓¬1␈↓α ... x␈↓¬n␈↓α:e␈↓␈α
is␈α
assigned␈αtrue␈α
if␈α
and␈αonly␈α
if␈α
␈↓αe␈↓␈α
is␈αassigned␈α
true␈α
for␈αall␈α
assignments␈α
of␈αelements␈α
of
␈↓ ↓H␈↓the␈α∞domain␈α∞to␈α∞the␈α∞␈↓αx␈↓'s.␈α∞ If␈α∞␈↓αe␈↓␈α∞has␈α∞free␈α∞variables␈α∞that␈α∞are␈α∞not␈α∞among␈α∞the␈α∞␈↓αx␈↓'s,␈α∞then␈α∞the␈α∞truth␈α∞of␈α
the
␈↓ ↓H␈↓sentence␈αdepends␈αon␈αthe␈αvalues␈αassigned␈αto␈αthese␈αremaining␈αfree␈αvariables.␈α ␈↓α∃x␈↓¬1␈↓α ... x␈↓¬n␈↓α:e␈↓␈αis␈αassigned
␈↓ ↓H␈↓true␈αif␈αand␈αonly␈αif␈α␈↓αe␈↓␈αis␈αassigned␈αtrue␈αfor␈α␈↓αsome␈↓␈αassignment␈αof␈αvalues␈αin␈αthe␈αdomain␈αto␈αthe␈α␈↓αx␈↓'s.␈α Free
␈↓ ↓H␈↓variables are handled just as before.

␈↓ ↓H␈↓        ␈↓αλx␈↓¬1␈↓α ... x␈↓¬n␈↓α:u␈↓␈α∩is␈α∩assigned␈α⊃a␈α∩function␈α∩or␈α∩predicate␈α⊃according␈α∩to␈α∩whether␈α∩␈↓αu␈↓␈α⊃is␈α∩a␈α∩term␈α∩or␈α⊃a
␈↓ ↓H␈↓sentence.␈α∞ The␈α∞value␈α∂of␈α∞␈↓α[λx␈↓¬1␈↓α ... x␈↓¬n␈↓α:u][t␈↓¬1␈↓α,...,t␈↓¬n␈↓α]␈α∞is␈α∂obtained␈α∞by␈α∞evaluating␈α∂the␈α∞t␈↓'s␈α∞and␈α∂using␈α∞these
␈↓ ↓H␈↓values␈αas␈αvalues␈α
of␈αthe␈α␈↓αx␈↓'s␈αin␈α
the␈αevaluation␈αof␈α
␈↓αu␈↓.␈α If␈α␈↓αu␈↓␈αhas␈α
free␈αvariables␈αin␈α
addition␈αto␈αthe␈α␈↓αx␈↓'s,␈α
the
␈↓ ↓H␈↓function assigned will depend on them too.

␈↓ ↓H␈↓        Those␈αwho␈αare␈αfamiliar␈αwith␈αthe␈αlambda␈αcalculus␈αshould␈αnote␈αthat␈αλ␈αis␈αbeing␈αused␈αhere␈αin␈αa
␈↓ ↓H␈↓very␈αlimited␈αway.␈α Namely,␈αthe␈αvariables␈αin␈αa␈αlambda-expression␈αtake␈αonly␈αelements␈αof␈αthe␈αdomain
␈↓ ↓H␈↓as␈α
values,␈α
whereas␈αthe␈α
essence␈α
of␈α
the␈αlambda␈α
calculus␈α
is␈α
that␈αthey␈α
take␈α
arbitrary␈α
functions␈αas␈α
values.
␈↓ ↓H␈↓We may call these restricted lambda expressions ␈↓αfirst order lambdas␈↓.



␈↓ ↓H␈↓2.  ␈↓βConditional forms.␈↓


␈↓ ↓H␈↓        All the properties we shall use of conditional forms follow from the relation

␈↓ ↓H␈↓        ␈↓α[p ⊃ [␈↓βif␈↓α p ␈↓βthen ␈↓αa ␈↓βelse␈↓α b] = a] ∧ [¬p ⊃ [␈↓βif␈↓α p ␈↓βthen␈↓α a ␈↓βelse␈↓αb] = b]␈↓.

␈↓ ↓H␈↓(If␈α
we␈α
weren't␈α
adhering␈αto␈α
the␈α
requireement␈α
that␈αall␈α
terms␈α
be␈α
defined␈αfor␈α
all␈α
values␈α
of␈αthe␈α
variables,
␈↓ ↓H␈↓the situation would be more complicated).

␈↓ ↓H␈↓        It is, however, worthwhile to list separately some properties of conditional forms.

␈↓ ↓H␈↓        First we have the obvious

␈↓ ↓H␈↓        ␈↓βif␈↓∧ T ␈↓βthen␈↓α a ␈↓βelse␈↓α b = a␈↓

␈↓ ↓H␈↓and

␈↓ ↓H␈↓        ␈↓βif␈↓∧ F ␈↓βthen␈↓α a ␈↓βelse␈↓α b = b␈↓.
␈↓ ↓H␈↓␈↓ ¬wCHAPTER I␈↓ I4


␈↓ ↓H␈↓        Next we have a ␈↓αdistributive law␈↓ for functions applied to conditional forms, namely

␈↓ ↓H␈↓        ␈↓αf[␈↓βif␈↓α p ␈↓βthen␈↓α a ␈↓βelse␈↓α b] = ␈↓βif␈↓α p ␈↓βthen␈↓α f[a] ␈↓βelse␈↓α f[b]␈↓.

␈↓ ↓H␈↓This␈αapplies␈αto␈αpredicates␈αas␈αwell␈αas␈αfunctions␈αand␈αcan␈αalso␈αbe␈αused␈αwhen␈αone␈αof␈αthe␈αarguments␈αof
␈↓ ↓H␈↓a␈αfunction␈αof␈α
several␈αarguments␈αis␈αa␈α
conditional␈αform.␈α It␈α
also␈αapplies␈αwhen␈αone␈α
of␈αthe␈αterms␈α
of␈αa
␈↓ ↓H␈↓conditional form is itself a conditional form.

␈↓ ↓H␈↓Thus

␈↓ ↓H␈↓        ␈↓βif␈↓α [␈↓βif␈↓α p ␈↓βthen␈↓α q ␈↓βelse␈↓α r] ␈↓βthen␈↓α a ␈↓βelse␈↓α b = ␈↓βif␈↓α p ␈↓βthen␈↓α [␈↓βif␈↓α q ␈↓βthen␈↓α a ␈↓βelse␈↓α b] ␈↓βelse␈↓α [␈↓βif␈↓α r ␈↓βthen␈↓α a ␈↓βelse␈↓α b]␈↓

␈↓ ↓H␈↓and

␈↓ ↓H␈↓        ␈↓βif␈↓α p ␈↓βthen␈↓α [␈↓βif␈↓α q ␈↓βthen␈↓α a ␈↓βelse␈↓α b] ␈↓βelse␈↓α c = ␈↓βif␈↓α q ␈↓βthen␈↓α [␈↓βif␈↓α p ␈↓βthen␈↓α a ␈↓βelse␈↓α c] ␈↓βelse␈↓α [␈↓βif␈↓α p ␈↓βthen␈↓α b ␈↓βelse␈↓α c]␈↓.

␈↓ ↓H␈↓        When␈α
the␈α
expressions␈α
following␈α
␈↓βthen␈↓␈α
and␈α
␈↓βelse␈↓␈α
are␈α
sentences,␈α
then␈α
the␈α
conditional␈α
form␈α
can
␈↓ ↓H␈↓be replaced by a sentence according to

␈↓ ↓H␈↓        ␈↓α[␈↓βif␈↓α p ␈↓βthen␈↓α q ␈↓βelse␈↓α r] ≡ [p ∧ q] ∨ [¬p ∧ r]␈↓.

␈↓ ↓H␈↓These␈αtwo␈αrules␈αpermit␈αeliminating␈αconditional␈αforms␈αfrom␈αsentences␈αby␈αfirst␈αusing␈αdistributivity␈αto
␈↓ ↓H␈↓move␈αthe␈αconditionals␈αto␈αthe␈α
outside␈αof␈αany␈αfunctions␈αand␈α
then␈αreplacing␈αthe␈αconditional␈αform␈αby␈α
a
␈↓ ↓H␈↓Boolean expression.

␈↓ ↓H␈↓        Note␈αthat␈αthe␈αelimination␈αof␈αconditional␈αforms␈αmay␈αincrease␈αthe␈αsize␈αof␈αa␈αsentence,␈αbecause␈α␈↓αp␈↓
␈↓ ↓H␈↓occurs␈α
twice␈α
in␈α
the␈α
right␈αhand␈α
side␈α
of␈α
the␈α
above␈α
equivalence.␈α In␈α
the␈α
most␈α
unfavorable␈α
case,␈α
␈↓αp␈↓␈αis
␈↓ ↓H␈↓dominates␈α∪the␈α∩size␈α∪of␈α∩the␈α∪expression␈α∩so␈α∪that␈α∩writing␈α∪it␈α∩twice␈α∪almost␈α∩doubles␈α∪the␈α∩size␈α∪of␈α∩the
␈↓ ↓H␈↓expression.

␈↓ ↓H␈↓        Suppose␈α
that␈α
␈↓αa␈↓␈αand␈α
␈↓αb␈↓␈α
in␈α
␈↓βif␈↓α p ␈↓βthen␈↓α a ␈↓βelse␈↓α b␈↓␈αare␈α
expressions␈α
that␈αmay␈α
contain␈α
the␈α
sentence␈α␈↓αp␈↓.
␈↓ ↓H␈↓Occurrences␈αof␈α␈↓αp␈↓␈αin␈α␈↓αa␈↓␈αcan␈αbe␈αreplaced␈αby␈α␈↓∧T␈↓,␈αand␈αoccurrences␈αof␈α␈↓αp␈↓␈αin␈α␈↓αb␈↓␈αcan␈αbe␈αreplaced␈αby␈α␈↓∧F␈↓.␈α This
␈↓ ↓H␈↓follows from the fact that ␈↓αa␈↓ is only evaluated if ␈↓αp␈↓ is true and ␈↓αb␈↓ is evaluated only if ␈↓αp␈↓ is false.

␈↓ ↓H␈↓        This␈α⊃leads␈α⊂to␈α⊃a␈α⊂strengthened␈α⊃form␈α⊂of␈α⊃the␈α⊂law␈α⊃of␈α⊂replacement␈α⊃of␈α⊂equals␈α⊃by␈α⊃equals.␈α⊂ The
␈↓ ↓H␈↓ordinary␈αform␈αof␈αthe␈αlaw␈αsays␈α
that␈αif␈αwe␈αhave␈α␈↓αe = e'␈↓,␈αthen␈αwe␈α
can␈αreplace␈αany␈αoccurrence␈αof␈α␈↓αe␈↓␈αin␈α
an
␈↓ ↓H␈↓expression␈α∩by␈α∩an␈α∩occurrence␈α∩of␈α⊃␈↓αe'␈↓.␈α∩ However,␈α∩if␈α∩we␈α∩want␈α∩to␈α⊃replace␈α∩␈↓αe␈↓␈α∩by␈α∩␈↓αe'␈↓␈α∩within␈α∩␈↓αa␈↓␈α⊃within
␈↓ ↓H␈↓␈↓βif␈↓α p ␈↓βthen␈↓α a ␈↓βelse␈↓α b␈↓,␈α∂then␈α∞we␈α∂need␈α∞only␈α∂prove␈α∞␈↓αp ⊃ e =e'␈↓,␈α∂and␈α∞to␈α∂make␈α∞the␈α∂replacement␈α∞within␈α∂␈↓αb␈↓␈α∞we
␈↓ ↓H␈↓need only prove ␈↓α¬p ⊃ e = e'␈↓.

␈↓ ↓H␈↓        Additional␈α∃facts␈α∃about␈α∃conditional␈α∃forms␈α∃are␈α∃given␈α∃in␈α∃(McCarthy␈α∃1963a)␈α⊗including␈α∃a
␈↓ ↓H␈↓discussion␈αof␈α
canonical␈αforms␈α
that␈αparallels␈αthe␈α
canonical␈αforms␈α
of␈αBoolean␈α
forms.␈α Any␈αquestion␈α
of
␈↓ ↓H␈↓equivalence␈α⊂of␈α⊂conditional␈α∂forms␈α⊂is␈α⊂decidable␈α∂by␈α⊂truth␈α⊂tables␈α∂analogously␈α⊂to␈α⊂the␈α⊂decidability␈α∂of
␈↓ ↓H␈↓Boolean forms.
␈↓ ↓H␈↓␈↓ ¬wCHAPTER I␈↓ I5


␈↓ ↓H␈↓3.  ␈↓βLambda-expressions.␈↓


␈↓ ↓H␈↓        The␈α∞only␈α∞additional␈α∞rule␈α∞required␈α∞for␈α∞handlying␈α∞lambda-expressions␈α∞in␈α∞first␈α∞order␈α∞logic␈α
is
␈↓ ↓H␈↓called ␈↓αlambda-conversion␈↓, essentially

␈↓ ↓H␈↓        ␈↓α[λx:e][a] =␈↓ <the result of substituting ␈↓αe␈↓ for ␈↓αx␈↓ in ␈↓αa␈↓>.

␈↓ ↓H␈↓As examples of this rule, we have

␈↓ ↓H␈↓        ␈↓α[λx:␈↓βa␈↓α x . y][u . v] = [␈↓βa␈↓α[u . v]] . y␈↓.

␈↓ ↓H␈↓However,␈α∞a␈α∞complication␈α
requires␈α∞modifying␈α∞the␈α
rule.␈α∞ Namely,␈α∞we␈α
can't␈α∞substitute␈α∞for␈α∞a␈α
variable
␈↓ ↓H␈↓and␈αexpression␈αthat␈αhas␈αa␈αfree␈αvariable␈αinto␈αa␈αcontext␈αin␈αwhich␈αthat␈αfree␈αvariable␈αis␈αbound.␈α Thus
␈↓ ↓H␈↓it␈α⊂would␈α⊂be␈α⊂wrong␈α⊂to␈α⊂substitute␈α⊂␈↓αx + y␈↓␈α⊃for␈α⊂␈↓αx␈↓␈α⊂in␈α⊂␈↓α∀y:[x + y = z]␈↓␈α⊂or␈α⊂into␈α⊂the␈α⊃term␈α⊂␈↓α[λy:x + y][u + v]␈↓.
␈↓ ↓H␈↓Before␈α
doing␈α
the␈αsubstitution,␈α
the␈α
variable␈α␈↓αy␈↓␈α
would␈α
have␈αto␈α
be␈α
replaced␈αin␈α
all␈α
its␈αbound␈α
occurrences
␈↓ ↓H␈↓by a fresh variable.

␈↓ ↓H␈↓        Lambda-expressions␈α⊗can␈α⊗always␈α⊗be␈α⊗eliminated␈α⊗from␈α⊗sentences␈α⊗and␈α⊗terms␈α⊗by␈α∃lambda-
␈↓ ↓H␈↓conversion,␈αbut␈αthe␈αexpression␈αmay␈αincrease␈αgreatly␈αin␈αlength␈αif␈αa␈αlengthy␈αterm␈αreplaces␈αa␈αvariable
␈↓ ↓H␈↓that␈α∂occurs␈α∂more␈α∞than␈α∂once␈α∂in␈α∞␈↓αe␈↓.␈α∂ It␈α∂is␈α∞easy␈α∂to␈α∂make␈α∞an␈α∂expression␈α∂of␈α∞length␈α∂␈↓αn␈↓␈α∂whose␈α∂length␈α∞is
␈↓ ↓H␈↓increased to 2␈↓εn␈↓ by converting its ␈↓αn␈↓ nested lambda-expressions.



␈↓ ↓H␈↓4.  ␈↓βAlgebraic axioms for S-expressions and lists.␈↓


␈↓ ↓H␈↓        The␈α⊂algebraic␈α⊂facts␈α⊂about␈α⊂S-expressions␈α⊂are␈α∂expressed␈α⊂by␈α⊂the␈α⊂following␈α⊂sentences␈α⊂of␈α∂first
␈↓ ↓H␈↓order logic:

␈↓ ↓H␈↓        ␈↓α∀x.(issexp x ⊃ ␈↓βat␈↓α x ∨ (issexp ␈↓βa␈↓α x ∧ issexp ␈↓βd␈↓α x ∧ x = (␈↓βa␈↓α x . ␈↓βd␈↓α x)))␈↓

␈↓ ↓H␈↓and

␈↓ ↓H␈↓        ␈↓α∀x y.(issexp x ∧ issexp y ⊃ issexp(x.y) ∧ ¬␈↓βat␈↓α(x.y) ∧ x = ␈↓βa␈↓α(x.y) ∧ y = ␈↓βd␈↓α(x.y))␈↓.

␈↓ ↓H␈↓Here␈α
␈↓αissexp␈α
e␈↓␈αasserts␈α
that␈α
the␈α
object␈α␈↓αe␈↓␈α
is␈α
an␈αS-expression␈α
so␈α
that␈α
the␈αsentences␈α
used␈α
in␈α
proving␈αa
␈↓ ↓H␈↓particular␈α∞program␈α
correct␈α∞can␈α
involve␈α∞other␈α
kinds␈α∞of␈α∞entities␈α
as␈α∞well.␈α
 If␈α∞we␈α
can␈α∞assume␈α∞that␈α
all
␈↓ ↓H␈↓objects␈α
are␈α
S-expressions␈α
or␈α∞can␈α
declare␈α
certain␈α
variables␈α∞as␈α
ranging␈α
only␈α
over␈α∞S-expressions,␈α
we
␈↓ ↓H␈↓can simplify the axioms to

␈↓ ↓H␈↓        ␈↓α∀x.[␈↓βat␈↓α x ∨ x = [␈↓βa␈↓α x . ␈↓βd␈↓α x]]␈↓

␈↓ ↓H␈↓and

␈↓ ↓H␈↓        ␈↓α∀x y.[¬␈↓βat␈↓α[x.y] ∧ x = ␈↓βa␈↓α[x.y] ∧ y = ␈↓βd␈↓α[x.y]]␈↓.
␈↓ ↓H␈↓␈↓ ¬wCHAPTER I␈↓ I6


␈↓ ↓H␈↓        The algebraic facts about lists are expressed by the following sentences of first order logic:

␈↓ ↓H␈↓        ␈↓α∀x. islist x ⊃ x = ␈↓∧NIL␈↓α ∨ islist ␈↓βd ␈↓αx␈↓,

␈↓ ↓H␈↓        ␈↓α∀x y. islist y ⊃ islist[x . y]␈↓,

␈↓ ↓H␈↓        ␈↓α∀x y. islist y ⊃ ␈↓βa␈↓α[x . y] = x ∧ ␈↓βd␈↓α[x.y] = y␈↓.

␈↓ ↓H␈↓We␈α
can␈α
rarely␈α
assume␈αthat␈α
everything␈α
is␈α
a␈αlist,␈α
because␈α
the␈α
lists␈αusually␈α
contain␈α
atoms␈α
which␈αare␈α
not
␈↓ ↓H␈↓themselves lists.

␈↓ ↓H␈↓        These␈α∞axioms␈α∞are␈α∞analogous␈α∞to␈α∞the␈α∞algebraic␈α∞part␈α∞of␈α∞Peano's␈α∞axioms␈α∞for␈α∂the␈α∞non-negative
␈↓ ↓H␈↓integers.␈α The␈α
analogy␈αcan␈α
be␈αmade␈α
clear␈αif␈α
we␈αwrite␈α
Peano's␈αaxioms␈α
using␈α␈↓αn'␈↓␈α
for␈αthe␈α
successor␈αof␈α
␈↓αn␈↓
␈↓ ↓H␈↓and ␈↓αn␈↓ε-␈↓ for the predecessor of ␈↓αn␈↓.  Peano's algebraic axioms then become

␈↓ ↓H␈↓        ␈↓α∀n: n' ≠ 0␈↓,

␈↓ ↓H␈↓        ␈↓α∀n: (n')␈↓ε-␈↓α = n␈↓,

␈↓ ↓H␈↓and

␈↓ ↓H␈↓        ␈↓α∀n: n ≠ 0 ⊃ (n␈↓ε-␈↓α)' = n␈↓.

␈↓ ↓H␈↓Integers␈αspecialize␈α lists␈α
if␈αwe␈αidentify␈α0␈α
with␈α␈↓∧NIL␈↓␈αand␈α
assume␈αthat␈αthere␈αis␈α
only␈αone␈αobject␈α
(say␈α1)
␈↓ ↓H␈↓that can serve as a list element.  Then ␈↓αn' = cons[1,n]␈↓, and ␈↓αn␈↓ε-␈↓α = ␈↓βd␈↓α n␈↓.

␈↓ ↓H␈↓        Clearly␈α∂S-expressions␈α∂and␈α∂lists␈α∂satisfy␈α∂the␈α∂axioms␈α∂given␈α∂for␈α∂them,␈α∂but␈α∂unfortunately␈α∞these
␈↓ ↓H␈↓algebraic␈α∂axioms␈α⊂are␈α∂insufficient␈α∂to␈α⊂characterize␈α∂them.␈α⊂ For␈α∂example,␈α∂consider␈α⊂a␈α∂domain␈α⊂of␈α∂one
␈↓ ↓H␈↓element ␈↓↓a␈↓ satisfying

␈↓ ↓H␈↓        ␈↓βa␈↓α a = ␈↓βd␈↓α a = a . a = a␈↓.

␈↓ ↓H␈↓It␈α
satisfies␈α
the␈αalgebraic␈α
axioms␈α
for␈αS-expressions.␈α
 We␈α
can␈α
exclude␈αit␈α
by␈α
an␈αaxiom␈α
␈↓α∀x.(␈↓βa␈↓α␈α
x␈α
≠␈αx)␈↓,
␈↓ ↓H␈↓but␈α
this␈α∞won't␈α
exclude␈α
other␈α∞circular␈α
list␈α
structures␈α∞that␈α
eventually␈α
return␈α∞to␈α
the␈α
same␈α∞element␈α
by
␈↓ ↓H␈↓some␈α
␈↓βa-d␈↓␈αchain.␈α
 Actually␈α
we␈αwant␈α
to␈α
exclude␈αall␈α
infinite␈α
chains,␈αbecause␈α
most␈α
LISP␈αprograms␈α
won't
␈↓ ↓H␈↓terminate␈α∞unless␈α
every␈α∞␈↓βa-d␈↓␈α
chain␈α∞eventually␈α
terminates␈α∞in␈α
an␈α∞atom.␈α
 This␈α∞cannot␈α
be␈α∞done␈α∞by␈α
any
␈↓ ↓H␈↓finite set of axioms.



␈↓ ↓H␈↓5.  ␈↓βAxiom schemas of induction.␈↓


␈↓ ↓H␈↓        ␈α∞       In␈α
order␈α∞to␈α
exclude␈α∞infinite␈α
list␈α∞structures␈α
we␈α∞need␈α
axioms␈α∞of␈α
induction␈α∞analogous␈α
to
␈↓ ↓H␈↓Peano's induction axiom.  Peano's axiom is ordinarily written

␈↓ ↓H␈↓        ␈↓αP(0) ∧ ∀n:(P(n) ⊃ P(n')) ⊃ ∀n:P(n)␈↓.
␈↓ ↓H␈↓␈↓ ¬wCHAPTER I␈↓ I7


␈↓ ↓H␈↓Here␈α∞␈↓αP(n)␈↓␈α∞is␈α∞an␈α∞arbitrary␈α∞predicate␈α∞of␈α∞integers,␈α∞and␈α∞we␈α∞get␈α∞particular␈α∞instances␈α∞of␈α∞the␈α∞axiom␈α∞by
␈↓ ↓H␈↓substituting particular predicates.

␈↓ ↓H␈↓Peano's induction schema can also be written

␈↓ ↓H␈↓        ␈↓α∀n:(n = 0 ∨ P(n␈↓ε-␈↓α) ⊃ P(n)) ⊃ ∀n:P(n)␈↓,

␈↓ ↓H␈↓and the equivalence of the two forms is easily proved.

␈↓ ↓H␈↓        The S-expression analog is

␈↓ ↓H␈↓        ␈↓α∀x:[issexp x ⊃ [␈↓βat␈↓α x ∨ P[␈↓βa␈↓α x] ∧ P[␈↓βd␈↓α x] ⊃ P[x]]] ⊃ ∀x:[issexp x ⊃ P[x]]␈↓,

␈↓ ↓H␈↓or, assuming everything is an S-expression

␈↓ ↓H␈↓        ␈↓α∀x:[␈↓βat␈↓α x ∨ P[␈↓βa␈↓α x] ∧ P[␈↓βd␈↓α x] ⊃ P[x]] ⊃ ∀x:P[x]␈↓.

␈↓ ↓H␈↓        The corresponding axiom schema for lists is

␈↓ ↓H␈↓        ␈↓α∀u:[islist u ⊃ [␈↓βn␈↓α u ∨ P[␈↓βd␈↓α u] ⊃ P[u]]] ⊃ ∀u:[islist u ⊃ P[u]]␈↓.

␈↓ ↓H␈↓        These␈α⊂schemas␈α⊂are␈α⊂called␈α∂principles␈α⊂of␈α⊂␈↓αstructural␈α⊂induction␈↓,␈α∂since␈α⊂the␈α⊂induction␈α⊂is␈α⊂on␈α∂the
␈↓ ↓H␈↓structure of the entities involved.



␈↓ ↓H␈↓6.  ␈↓βProofs by structural induction.␈↓


␈↓ ↓H␈↓        Recall that the operation of appending two lists is defined by

␈↓ ↓H␈↓␈↓α1.1)␈↓ α8 u * v ← ␈↓βif n␈↓α u ␈↓βthen␈↓α v ␈↓βelse a␈↓α u . [␈↓βd␈↓α u * v]␈↓.

␈↓ ↓H␈↓Because␈α
␈↓αu*v␈↓␈α
is␈α
defined␈α
for␈α∞all␈α
␈↓αu␈↓␈α
and␈α
␈↓αv␈↓,␈α
i.e.␈α
the␈α∞computation␈α
described␈α
above␈α
terminates␈α
for␈α∞all␈α
␈↓αu␈↓
␈↓ ↓H␈↓and ␈↓αv␈↓, we can replace (1.1) by the sentence

␈↓ ↓H␈↓␈↓α1.2)␈↓ α8 ∀u v:[islist u ∧ islist v ⊃ [u * v = ␈↓βif n␈↓α u ␈↓βthen␈↓α v ␈↓βelse a␈↓α u . [␈↓βd␈↓α u * v]]]␈↓.

␈↓ ↓H␈↓Now␈α
suppose␈αwe␈α
would␈αlike␈α
to␈αprove␈α
␈↓α∀v:[␈↓∧NIL␈↓α␈α*␈α
v␈α=␈α
v]␈↓.␈α This␈α
is␈αquite␈α
trivial;␈αwe␈α
need␈αonly␈α
substitute
␈↓ ↓H␈↓␈↓∧NIL␈↓ for ␈↓αx␈↓ in (1.2), getting

␈↓ ↓H␈↓␈↓ αG␈↓∧NIL␈↓α * v ␈↓ β( = ␈↓βif n ␈↓∧NIL ␈↓βthen␈↓α v ␈↓βelse a ␈↓∧NIL␈↓α . [␈↓βd ␈↓∧NIL␈↓α * v]

␈↓ ↓H␈↓α␈↓ β( = v␈↓.

␈↓ ↓H␈↓Next␈αconsider␈αproving␈α␈↓α∀u:[u␈α*␈α␈↓∧NIL␈↓α␈α
=␈αu]␈↓.␈α This␈αcannot␈αbe␈αdone␈α
by␈αsimple␈αsubstitution,␈αbut␈αit␈αcan␈α
be
␈↓ ↓H␈↓done as follows:  First substitute ␈↓αλu:[u * ␈↓∧NIL␈↓α = u]␈↓ for ␈↓αP␈↓ in the induction schema
␈↓ ↓H␈↓␈↓ ¬wCHAPTER I␈↓ I8


␈↓ ↓H␈↓        ␈↓α∀u:[islist u ⊃ [␈↓βn␈↓α u ∨ P[␈↓βd␈↓α u] ⊃ P[u]]] ⊃ ∀u:[islist u ⊃ P[u]]␈↓,

␈↓ ↓H␈↓getting

␈↓ ↓H␈↓        ␈↓α∀u:[islist␈α
u␈α⊃␈α
[␈↓βn␈↓α␈α
u␈α∨␈α
λu:[u␈α*␈α
␈↓∧NIL␈↓α␈α
=␈αu][␈↓βd␈↓α␈α
u]␈α
⊃␈αλu:[u␈α
*␈α␈↓∧NIL␈↓α␈α
=␈α
u][u]]]␈α⊃␈α
∀u:[islist␈α
u␈α⊃␈α
λu:[u␈α*␈α
␈↓∧NIL␈↓α
␈↓ ↓H␈↓α= u][u]]␈↓.

␈↓ ↓H␈↓Carrying out the indicated lambda conversions makes this

␈↓ ↓H␈↓␈↓α1.3)␈↓ α8 ∀u:[islist u ⊃ [␈↓βn␈↓α u ∨ ␈↓βd␈↓α u * qNIL = ␈↓βd␈↓α u] ⊃ u * qNIL = u] ⊃ ∀u:[islist u ⊃ u * qNIL = u]␈↓.